abstract sig ServizioBase {}

sig Volo, Hotel, Escursione extends ServizioBase {}

//signature che rappresenta il pacchetto offerto dall'agenzia
sig PacchettoOfferto {
	voloPacchetto:  one Volo,
	hotelPacchetto: one Hotel,
	escursionePacchetto: some Escursione
}


fact {
	all p, p':PacchettoOfferto | p != p' and p.voloPacchetto = p'.voloPacchetto and
					p.escursionePacchetto = p'.escursionePacchetto =>	p.hotelPacchetto != p'.hotelPacchetto
}

fact {
	all p, p':PacchettoOfferto | p != p' and p.voloPacchetto = p'.voloPacchetto and
						p.hotelPacchetto = p'.hotelPacchetto =>p.escursionePacchetto = p'.escursionePacchetto 
}

fact {
	all p, p':PacchettoOfferto | p != p' and p.hotelPacchetto = p'.hotelPacchetto and
					p.escursionePacchetto = p'.escursionePacchetto =>p.voloPacchetto != p'.voloPacchetto	
}


//Asserzione che verifica che due pacchetti siano distinti (non abbiano gli stessi volo, hotel, escursioni)

assert pacchettoNonDuplicato {

	no p, p':PacchettoOfferto | p != p' and p.voloPacchetto = p'.voloPacchetto and
					p.escursionePacchetto = p'.escursionePacchetto and
					p.hotelPacchetto = p'.hotelPacchetto
}


check pacchettoNonDuplicato
